\begin{tabbing}
$\forall$\=$A$:Type, $I$:MaInterface($A$), $l$:IdLnk, ${\it tg}$:Id,\+
\\[0ex]${\it nmr}$:Namer(2;[${\it tg}$; lname($l$)] @ ma{-}interface{-}tags($I$)).
\-\\[0ex]Normal($A$,$I$)
\\[0ex]$\Rightarrow$ gluable($I$;$l$;${\it tg}$)
\\[0ex]$\Rightarrow$ gluable2($A$;$I$;$l$;${\it tg}$)
\\[0ex]$\Rightarrow$ \=($\forall$$k$:Knd.\+
\\[0ex]($k$ $\in$ fpf{-}domain($\oplus$(mapl($\lambda$$i$.if $i$ = source($l$)
\\[0ex]then ma{-}interface{-}conds($I$;$i$)
\\[0ex]else es{-}in{-}port{-}conds($A$;(link ${\it nmr}$(0) from $i$ to source($l$));${\it nmr}$(1))
\\[0ex]fi ;remove{-}repeats(IdDeq;ma{-}interface{-}locs($I$))))))
\\[0ex]$\Rightarrow$ \=((\=$\oplus$(mapl($\lambda$$i$.if $i$ = source($l$)\+\+
\\[0ex]then ma{-}interface{-}conds($I$;$i$)
\\[0ex]else es{-}in{-}port{-}conds($A$;(link ${\it nmr}$(0) from $i$ to source($l$));${\it nmr}$(1))
\\[0ex]fi ;remove{-}repeats(IdDeq;ma{-}interface{-}locs($I$))))($k$).1)
\-\\[0ex]\& ($\neg$($k$ = rcv($l$,${\it tg}$)))))
\-\-
\end{tabbing}